Nuprl Definition : normal-da
0,22
postcript
pdf
Normal(
da
) ==
x
dom(
da
).
A
=
da
(
x
)
Normal(
A
)
latex
clarification:
normal-da{i:l}(
da
) == fpf-all(Knd; KindDeq;
da
;
x
,
A
.normal-type{i:l}(
A
))
latex
Definitions
x
dom(
f
).
v
=
f
(
x
)
P
(
x
;
v
)
,
Knd
,
KindDeq
,
Normal(
T
)
FDL editor aliases
normal-da
origin
x
dom(da). A=da(x) 
Normal(A)
xdom(da). A=da(x) Normal(A)
xdom(f). v=f(x) P(x;v)